Inference at * 2 
Iof proof for Lemma equal-bnot:



1. x : 
2. y : 
3. (y)
4. (x)
  x 

latex

 by SupposeNot 

latex

 .

Definitions	x:A. B(x), Dec(P), P  Q, left + right, A, P  Q, False
Lemmas	decidable assert